Termination Proof Script
Consider the TRS R consisting of the rewrite rule
1:
a
(
b
(
a
(x)))
→
b
(
a
(x))
There are no dependency pairs. Hence the TRS is trivially terminating.
Tyrolean Termination Tool
(0.01 seconds) --- May 4, 2006